/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXI30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=XMAS25



␈↓ α∧␈↓α␈↓ ∧≤FUNCTIONS CHARACTERIZING FLOW CHARTS

␈↓ α∧␈↓␈↓ αTWhen␈α
one␈αstudies␈α
programs␈α
organized␈αas␈α
flow␈α
charts,␈αone␈α
is␈α
inclined␈αto␈α
prefer␈α
flow␈αcharts
␈↓ α∧␈↓with␈αa␈αsingle␈αentry␈αand␈αa␈αsingle␈αexit.␈α However,␈αthe␈αoperations␈αof␈αbuilding␈αflow␈αcharts␈αfrom␈αparts
␈↓ α∧␈↓inevitably involve flow charts with multiple entries and ultiple exits.

␈↓ α∧␈↓␈↓ αTOur␈α
approach␈α
is␈αto␈α
characterize␈α
flow␈αcharts␈α
by␈α
certain␈αfunctions␈α
and␈α
show␈αhow␈α
to␈α
get␈αthe
␈↓ α∧␈↓functions␈αcharacterizing␈α
new␈αflow␈α
charts␈αfrom␈α
those␈αcharacterizing␈α
the␈αflow␈α
charts␈αfrom␈αwhich␈α
the
␈↓ α∧␈↓new␈α
ones␈α
are␈α
formed.␈α
 This␈αis␈α
in␈α
contrast␈α
with␈α
the␈α
approach␈αof␈α
Ianov␈α
as␈α
described␈α
in␈α(Ianov␈α
1959)
␈↓ α∧␈↓and␈α∪(Rutledge␈α∪1964).␈α∪ Our␈α∪reason␈α∪is␈α∀that␈α∪mathematics␈α∪provides␈α∪us␈α∪with␈α∪powerful␈α∀tools␈α∪for
␈↓ α∧␈↓manipulating␈α⊃functions,␈α⊃and,␈α⊂moreover,␈α⊃facts␈α⊃about␈α⊂flow␈α⊃charts␈α⊃must␈α⊂be␈α⊃combined␈α⊃with␈α⊂other
␈↓ α∧␈↓mathematical facts which are most conveniently decribed in terms of functions, predicates and sets.


␈↓ α∧␈↓α␈↓ αT1. Flow chart functions

␈↓ α∧␈↓␈↓ αTFigure␈α∂1␈α∂represents␈α∂a␈α∂flow␈α∂chart␈α∂␈↓↓c␈↓␈α∂whose␈α∞inner␈α∂workings␈α∂we␈α∂do␈α∂not␈α∂wish␈α∂to␈α∂specify,␈α∞but
␈↓ α∧␈↓whose␈α∞behavior␈α
we␈α∞wish␈α
to␈α∞characterize␈α
by␈α∞functions.␈α
 The␈α∞arrows␈α
into␈α∞the␈α
␈↓↓blob␈↓␈α∞represent␈α
paths
␈↓ α∧␈↓along␈α
which␈α
control␈α
enters␈α
the␈α
flow␈α
chart␈α(called␈α
entries),␈α
and␈α
the␈α
arrows␈α
out␈α
represent␈α
paths␈αby
␈↓ α∧␈↓which␈αcontrol␈αleaves␈αit␈α(called␈α
␈↓↓exits).␈↓␈αLet␈α␈↓↓En(c)␈↓␈αbe␈αthe␈α
set␈αof␈αentries␈αof␈α␈↓↓c,␈↓␈α
and␈αlet␈α␈↓↓Ex(c)␈↓␈αbe␈αits␈αset␈α
of
␈↓ α∧␈↓exits.␈α Let␈α␈↓↓x␈↓␈αrepresent␈αthe␈αstate␈αvector,␈αi.e.␈α the␈αcollection␈αof␈αassignments␈αof␈αvalues␈αto␈αthe␈αvariables
␈↓ α∧␈↓occurring␈α∞in␈α∞the␈α∞program.␈α∞ We␈α∞define␈α∞predicates␈α∞␈↓↓p␈↓βij␈↓↓(x,c)␈↓β␈α∞where␈α∞␈↓↓i␈↓β␈α∞ranges␈α∞over␈α∞␈↓↓En(c)␈↓β␈α∞and␈α∞␈↓↓j␈α∞ranges␈↓β␈α∞over
␈↓ α∧␈↓β␈↓↓Ex(c),␈↓β and functions ␈↓↓s␈↓βi␈↓↓(x,c)␈↓β where ␈↓↓i␈↓β again ranges over ␈↓↓En(c)␈↓β as follows:

␈↓ α∧␈↓β␈↓ αT(i)␈α	␈↓↓p␈↓βij␈↓↓(x,c)␈↓β␈αλis␈α	true␈α	if␈αλand␈α	only␈α	if␈αλentering␈α	the␈α	flow␈αλchart␈α	␈↓↓c␈↓β␈α	at␈αλentry␈α	␈↓↓i␈↓β␈α	with␈αλinitial␈α	state␈α	␈↓↓x␈↓β␈αλresults␈α	in␈α	leaving␈αλthe␈α	flow␈α	chart␈αλat
␈↓ α∧␈↓βexit␈α	␈↓↓j.␈αλ ␈↓β␈α	(ii)␈αλ␈↓↓s␈↓βi␈↓↓(x,c)␈↓β␈α	is␈αλthe␈α	value␈αλof␈α	the␈α	state␈αλat␈α	exit␈αλfrom␈α	the␈αλflow␈α	chart␈αλwhen␈α	it␈αλis␈α	entered␈α	at␈αλ␈↓↓i␈↓β␈α	with␈αλinitial␈α	state␈αλ␈↓↓x.␈↓β␈α	Note␈αλthat␈α	␈↓↓s␈↓β␈α	is␈αλa
␈↓ α∧␈↓βpartial functions, because the program may never exit.

␈↓ α∧␈↓β␈↓ αTObviously␈α
the␈α	predicates␈α
␈↓↓p␈↓βij␈↓␈α
and␈α	the␈α
functions␈α
␈↓↓s␈↓βi␈↓␈α	characterize␈α
the␈α	flow␈α
chart␈α
␈↓↓c,␈↓␈α	because␈α
if␈α
one␈α	knows
␈↓ α∧␈↓these␈αone␈αknows␈α
where␈αthe␈αprogram␈α
will␈αexit␈αand␈α
what␈αthe␈αnew␈α
state␈αwill␈αbe␈α
for␈αany␈αentrance␈α
into
␈↓ α∧␈↓the flow chart.

␈↓ α∧␈↓␈↓ αTIf␈αwe␈αsuppose␈α
that␈αthe␈αflow␈αchart␈α
is␈αultimately␈αconstructed␈α
out␈αof␈αelementary␈αcompute␈α
blocks
␈↓ α∧␈↓and␈αelementary␈αdecision␈αblocks,␈αone␈αneeds␈αto␈αshow␈αhow␈αto␈αwrite␈αthe␈α␈↓↓p␈↓'s␈αand␈α␈↓↓s␈↓'s␈αfor␈αthese␈αelements
␈↓ α∧␈↓and␈αthen␈αhow␈αto␈αget␈αthe␈α␈↓↓p␈↓'s␈αand␈α␈↓↓s␈↓'s␈αfor␈αa␈αcombination␈αof␈αblocks␈αfrom␈αthose␈αof␈αits␈αparts.␈α The␈αfirst
␈↓ α∧␈↓part␈αis␈αtrivial.␈α A␈αcompute␈αblock␈αhas␈αjust␈αone␈αentry␈α
and␈αone␈αexit,␈αso␈αthere␈αis␈αjust␈αone␈α␈↓↓p␈↓␈αand␈α
it␈αis
␈↓ α∧␈↓identically␈αtrue,␈αand␈αthere␈αis␈αjust␈αone␈α␈↓↓s,␈↓␈αand␈αit␈αis␈αjust␈αthe␈αfunction␈αof␈αtate␈αcomputed␈αby␈αthe␈αblock.
␈↓ α∧␈↓A␈α∞decision␈α∞block␈α∞has␈α∞one␈α∞entry␈α∞and␈α∞two␈α∞exits␈α
and␈α∞the␈α∞one␈α∞␈↓↓p␈↓␈α∞is␈α∞just␈α∞the␈α∞predicate␈α∞for␈α∞the␈α
YES
␈↓ α∧␈↓decision␈αand␈αthe␈αother␈αis␈αthe␈αpredicate␈αfor␈αthe␈αNO␈αdecision.␈α There␈αis␈αone␈α␈↓↓s,␈↓␈αand␈αit␈αis␈αthe␈αidentity
␈↓ α∧␈↓function.

␈↓ α∧␈↓␈↓ αTWe use the following operations that give new charts from old ones.

␈↓ α∧␈↓␈↓ αT(i)␈α
Suppression␈α
of␈α
an␈αentry␈α
␈↓↓i␈↓β0␈↓␈α
from␈α
a␈αchart␈α
␈↓↓c.␈↓␈α
This␈α
gives␈α
a␈αnew␈α
chart␈α
␈↓↓del(c,i␈↓β0␈↓↓)␈↓␈α
with␈αone␈α
fewer
␈↓ α∧␈↓entry, and whose ␈↓↓p␈↓'s and ␈↓↓s␈↓'s are the same as before except that the subscript ␈↓↓i␈↓β0␈↓ is omitted.

␈↓ α∧␈↓␈↓ αT(ii)␈α
Putting␈α
two␈α
charts␈α␈↓↓c1␈↓␈α
and␈α
␈↓↓c2␈↓␈α
side␈αby␈α
side.␈α
 Call␈α
the␈αnew␈α
chart␈α
␈↓↓c1∪ε2␈↓.␈α
 We␈αhave␈α
␈↓↓En(c1∪c2)
␈↓ α∧␈↓↓= En(c1)∪En(c2)␈↓, and ␈↓↓Ex(c1∪c2) = Ex(c1) ∪ Ex(c2)␈↓.  Moreover, we have


␈↓ α∧␈↓␈↓ ε|1␈↓ ∧
␈↓ α∧␈↓Flow Chart Functions␈↓ εJ␈↓πDraft␈↓␈↓ 
IMarch 5, 1976


␈↓ α∧␈↓␈↓ αT␈↓↓p␈↓βij␈↓↓(x,c1∪c2)␈α
=␈α␈↓αif␈↓↓␈α
i␈α
ε␈αc1␈α
␈↓αthen␈↓↓␈α
(␈↓αif␈↓↓␈αj␈α
ε␈α
c1␈α␈↓αthen␈↓↓␈α
p␈↓βij␈↓↓(x,c1)␈α␈↓αelse␈α
false)␈α
else␈α(if␈↓↓␈α
j␈α
ε␈αc1␈α
␈↓αthen␈α
false␈αelse
␈↓ α∧␈↓α␈↓↓p␈↓βij␈↓↓(x,c2))␈↓,

␈↓ α∧␈↓␈↓ αTand

␈↓ α∧␈↓␈↓ αT␈↓↓s␈↓βi␈↓↓(x,c1∪c2) = ␈↓αif␈↓↓ i ε c1 ␈↓αthen␈↓↓ s␈↓βi␈↓↓(x,c1) ␈↓αelse␈↓↓ p␈↓βi␈↓↓(x,c2)␈↓.

␈↓ α∧␈↓␈↓ αTBoth of these are trivial operations but the next is not.

␈↓ α∧␈↓␈↓ αT(iii)␈αConnecting␈α
the␈αexit␈α
␈↓↓m␈↓␈αto␈α
the␈αentry␈α
␈↓↓n␈αgiving␈↓␈α
a␈αnew␈α
chart␈α␈↓↓loop(c,m,n)␈↓␈α
with␈αone␈αfewer␈α
exit.
␈↓ α∧␈↓The␈α∞new␈α∂␈↓↓p␈↓'s␈α∞and␈α∂␈↓↓s␈↓'s␈α∞are␈α∞defined␈α∂by␈α∞the␈α∂recursion␈α∞equations␈α∞␈↓↓p␈↓βij␈↓↓(x,loop(c,m,n))␈α∂←␈α∞␈↓αif␈↓↓␈α∂p␈↓βin␈↓↓(x,c)␈α∞␈↓αthen␈↓↓
␈↓ α∧␈↓↓p␈↓βmj␈↓↓(s'(s␈↓βi␈↓↓(x,c),c,m,n),c) ␈↓αelse␈↓↓ p␈↓βij␈↓↓(x,c)␈↓,

␈↓ α∧␈↓␈↓ αTand

␈↓ α∧␈↓␈↓ αT␈↓↓s␈↓βi␈↓↓(x,loop(c,m,n)) ← ␈↓αif␈↓↓ p␈↓βin␈↓↓(x,c) ␈↓αthen␈↓↓ s␈↓βm␈↓↓(s'(s␈↓βi␈↓↓(x,c),c,m,n),c) ␈↓αelse␈↓↓ s␈↓βi␈↓↓(x,c)␈↓,

␈↓ α∧␈↓␈↓ αTwhere

␈↓ α∧␈↓␈↓ αT␈↓↓s'(x,c,m,n) ← ␈↓αif␈↓↓ p␈↓βmn␈↓↓(x,c) ␈↓αthen␈↓↓ s'(s␈↓βm␈↓↓(x,c),c,m,n) ␈↓αelse␈↓↓ x␈↓.

␈↓ α∧␈↓␈↓ αTA␈αlittle␈αcontemplation␈αwill␈αshow␈αthat␈αthis␈αrecursive␈αprocess␈αcaptures␈αour␈αintuitive␈α
notion␈αof
␈↓ α∧␈↓what␈αhappens␈αwhen␈αan␈αexit␈αis␈αconnected␈αto␈αan␈αentry.␈α If␈αwe␈αwere␈αusing␈αanother␈αformal␈αnotion␈αof
␈↓ α∧␈↓the␈α
computation␈α
performed␈α
by␈α
a␈α
flow␈α
chart,␈α∞then␈α
we␈α
would␈α
have␈α
to␈α
prove␈α
theorems␈α
in␈α∞order␈α
to
␈↓ α∧␈↓justify (i) - (iii).

␈↓ α∧␈↓␈↓ αTAn␈α⊂objective␈α∂worth␈α⊂undertaking␈α⊂is␈α∂to␈α⊂show␈α⊂that␈α∂any␈α⊂two␈α⊂equivalent␈α∂flow␈α⊂charts␈α⊂can␈α∂be
␈↓ α∧␈↓proved␈α∂equivalent␈α∂by␈α⊂the␈α∂theory␈α∂of␈α∂recursively␈α⊂defined␈α∂functions␈α∂from␈α∂these␈α⊂definitions.␈α∂ This
␈↓ α∧␈↓would␈α⊂be␈α⊂the␈α⊂analog␈α⊂of␈α⊃Ianov's␈α⊂theorem␈α⊂and␈α⊂ought␈α⊂to␈α⊃be␈α⊂based␈α⊂on␈α⊂a␈α⊂decision␈α⊃procedure␈α⊂for
␈↓ α∧␈↓recursions␈α
(possibly␈α
restricted␈αto␈α
iterative␈α
form)␈α
where␈αthere␈α
is␈α
only␈αone␈α
variable.␈α
 It␈α
would␈αhave
␈↓ α∧␈↓the␈αadvantage␈αover␈αthe␈αIanov␈αtheory␈αthat␈αit␈α
is␈αsimply␈αthe␈αtheory␈αof␈αrecursion␈αequations␈αapplied␈α
to
␈↓ α∧␈↓this case rather than an ad hoc confection.

␈↓ α∧␈↓␈↓ αTI␈α
don't␈α
know␈α
such␈α
a␈α
decision␈α
procedure,␈αnor␈α
has␈α
there␈α
been␈α
formulated␈α
a␈α
theory␈αof␈α
recursion
␈↓ α∧␈↓equations that is proved complete for this case.














␈↓ α∧␈↓␈↓ ε|2␈↓ ∧